Nuprl Definition : component-realizes
11,40
postcript
pdf
C
|-
es
,
in
,
out
.
P
(
es
;
in
;
out
)
==
X
:Interface(
ds
;
da
;
A
). let
R
,
Y
= (
C
(
X
)) in
R
|-
es
.es-decl(
es
;
ds
;
da
)
P
(
es
;[[
X
]];[[
Y
]])
latex
clarification:
component-realizes{i:l}
component-realizes
(
ds
;
da
;
A
;
B
;
C
;
es
,
in
,
out
.
P
(
es
;
in
;
out
))
==
X
:Interface(
ds
;
da
;
A
).
==
let
R
,
Y
= (
C
(
X
))
==
in
==
scheme-realizes{i:l}
== scheme-realizes
(
R
;
es
.(es-decl(
es
;
ds
;
da
)
P
(
es
;abs-interface(
es
;
X
);abs-interface(
es
;
Y
))))
latex
Definitions
[[
X
]]
,
es-decl(
es
;
ds
;
da
)
,
P
Q
,
S
|-
es
.
P
(
es
)
,
f
(
a
)
,
let
x
,
y
=
A
in
B
(
x
;
y
)
,
Interface(
ds
;
da
;
A
)
,
x
:
A
.
B
(
x
)
FDL editor aliases
component-realizes
origin